[model checking] A Kripke structure is a variation of nondeterministic automaton proposed by Saul Kripke, used in model checking to represent the behavior of a system. It is a simple abstract machine (a mathematical object) to capture the idea of a computing machine, without adding unnecessary complexities. It is basically a graph whose nod...